There Is No Preview Available For This Item
This item does not appear to have any files that can be experienced on Archive.org.
Please download files in this item to interact with them on your computer.
Show all files
In recent years, software model checking has been offered as a viable solution to the 'bug hunt' in software. Although only in its infancy, software model checking has shown promise in tackling this very difficult problem. In this talk, emphasis will be placed on the model checking within the verification process, whereby the abstracted Boolean program (modeled as a finite transition system) undergoes scrutiny. Conventional BDD-based model checking tools may suffer from space and/or computational limitations for large state spaces. Instead, we offer a new model checking paradigm that is based on SAT rather than BDDs.
While there has been some work on SAT-based state space traversal, they have been centered on the concept of 'blocking clauses', which is a direct derivation from conflict-driven learning in SAT solvers. On the other hand, we offer a completely different way of learning, in which knowledge is obtained from successes rather than conflicts. In our framework, equivalent search spaces form the knowledge base over which learning is performed. With our approach, significant space and time reductions are achieved, where conflict-driven methods could not. Our initial findings demonstrated that several orders of magnitude reduction in computation effort can be obtained.